The invention relates to the field of electronic design automation (EDA).
Sequential equivalence checking (SEC) may refer to verifying that the outputs of two hardware designs behave equivalently for any inputs sequence. In practice, SEC may be used to efficiently prove correctness of sequential design transformations, such as retiming, finite-state machine (FSM) re-encoding, addition of clock-gating logic, and/or the like.
Over the years, several different methodologies for SEC have been adopted, such as showing equivalence of two designs with respect to a specified initial state, such as the power-on reset state. This technique has attracted a lot of research and highly scalable algorithms are known.
Another example methodology considers completely random initial states. In this case, it is customary to perform an alignability analysis, that is, to look for a reset sequence that brings the random initial state to a deterministic synchronization state after which the designs behave equivalently. If a correct reset sequence is known, then the problem reduces to the previous one.
In general, alignability analysis is significantly less scalable and has several pitfalls. First, there is a risk of false negatives—comparing the design to itself could fail if the reset sequence does not exist. Second, there is a risk of false positives—for example, an automatically computed reset sequence may put a design into a deadlock state, and in this way two very different designs may behave identically. Another possibility is for the designer to specify a mapping file, correlating the initial values of the two designs.
The foregoing examples of the related art and limitations related therewith are intended to be illustrative and not exclusive. Other limitations of the related art will become apparent to those of skill in the art upon a reading of the specification and a study of the figures.